(declare-fun _substvar_80_ () Bool)
(declare-const r7 Real)
(push)
(pop)
(assert (exists ((q1 Bool) (q2 Bool) (q3 Real) (q4 Real) (q5 Real)) (=> (<= q3 4.0 q3) q1)))
(assert (exists ((q6 Real) (q7 Bool) (q8 Bool)) (<= 4.0 r7)))
(push)
(assert (not (forall ((q9 Real) (q10 Bool) (q11 Bool) (q12 Bool)) (=> (not q10) _substvar_80_))))
(push)
(push)
(assert (not (exists ((q13 Bool) (q14 Real) (q15 Real) (q16 Bool) (q17 Real)) (not (>= q14 880953340.0 q17 4.0)))))
(push)
(pop)
(pop)
(pop)
(assert (forall ((q45 Bool) (q46 Bool)) q45))
(pop)
(check-sat)
